library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.STD_LOGIC_ARITH.ALL;
use IEEE.STD_LOGIC_UNSIGNED.ALL;
entity formula is
    port(
        enable: in std_logic;
        reset: in std_logic;
        a: in std_logic_vector(3 downto 0);
        satisfied: out std_logic
    );
end entity formula;
architecture formula_behavior of formula is
signal sat_temp: std_logic := '0';
signal clause_signal: std_logic := '0';
signal formula_signal: std_logic := '0';
signal clause_literal : integer;
signal a_literal : std_logic := '0';
type formula is array(2 downto 0,3 downto 0) of integer;
signal f : formula := ((1,1,-1,0),(0,-1,1,1),(-1,0,0,-1));

begin
process(enable, reset)
begin --process
    if enable = '1' and reset ='0' then
		formula_signal <= '1';
		
         for i in 0 to 2 loop
			 
			 clause_signal <= '0';
			 
             for j in 0 to 3 loop
             
				 a_literal <= a(j);
				 clause_literal <= f(i,j);
				 
			 	 if clause_literal = -1 then
					  if a_literal = '0' then
						  clause_signal <= '1';
						  exit;
					  end if;
					  
				elsif clause_literal = 1 then
					if a_literal = '1' then
						clause_signal <= '1';
						exit;
					end if;
					
				end if;
					  
         end loop;
		
		 if clause_signal = '0' then
			 formula_signal <= '0';
			 exit;
			 
		end if;		 
      end loop;
	  
	  if formula_signal = '1' then
		  sat_temp <= '1';
		  
	   end if;
    elsif reset = '1' then
        sat_temp <= '0';
    end if;
end process;
satisfied <= sat_temp;
end architecture formula_behavior;